\n\n Ian P. Gent, Warwick Harvey, Tom Kelsey and Steve Linton. \"Generic SBDD\n using Computational Group Theory\". In Francesca Rossi, editor,\n Proceedings of the Ninth International Conference on Principles and\n Practice of Constraint Programming - CP 2003, LNCS 2833, pages\n 333-347. Springer-Verlag, 2003.
\n\n It has been enhanced by (amongst other things) being integrated with the\n symmetry expression library described in:
\n\n Warwick Harvey, Tom Kelsey and Karen Petrie. \"Symmetry Group Expression\n for CSPs.\" In Barbara Smith et al., editors, Proceedings of\n SymCon'03: Third International Workshop on Symmetry in Constraint\n Satisfaction Problems, a workshop of CP 2003, pages 86-96.\n September, 2003.
\n\n This library is still being developed and is expected to evolve.\n Feedback, suggestions, problem reports, etc. welcome.
\n\n Please note that this library currently does not work on Windows machines\n due to its dependence on the GAP interface library.
\n")). :- comment(see_also, [library(sym_expr), library(gap)]). :- comment(author, "Warwick Harvey, Steve Linton, Tom Kelsey, Ian Gent (and probably others...)"). :- comment(status, evolving). :- comment(struct(sbdd_shared), [summary : "Structure containing information for GAP-SBDD search", fields : [array : "Array of decision variables", depth : "Current depth of search tree", dec_info_list : "", dim_factors : "", val_offset : "", ground_points : "", throttle_pred : "", module : ""], desc : html(" Most of the contents of this structure are subject to change in future\n versions of the library and thus should not be accessed by user-level\n code. The user should also not change the contents of this structure!
\n")]). :- comment(all_solutions / 1, [summary : "Find all solutions to the given goal", args : ["Goal" : "The goal to execute"], amode : all_solutions(+), see_also : [all_solutions / 2, first_solution / 1], desc : html(" Finds all solutions for the goal Goal, and prints various statistics\n about the computation (CPU time taken, number of dominance checks\n performed, etc.).\n")]). :- comment(all_solutions / 2, [summary : "Find all solutions to the given goal", args : ["Goal" : "The goal to execute", "NSols" : "The number of solutions found"], amode : all_solutions(+, ?), see_also : [all_solutions / 1, first_solution / 1], desc : html(" Finds all solutions for the goal Goal, and prints various statistics\n about the computation (CPU time taken, number of dominance checks\n performed, etc.). The number of solutions found is unified with NSols.\n")]). :- comment(first_solution / 1, [summary : "Find the first solution to the given goal", args : ["Goal" : "The goal to execute"], amode : first_solution(+), see_also : [all_solutions / 1, all_solutions / 2], desc : html(" Finds the first solution for the goal Goal, and prints various statistics\n about the computation (CPU time taken, number of dominance checks\n performed, etc.).\n")]). :- comment(is_sbdd_var / 1, [summary : "Checks whether a variable is an SBDD variable", args : ["Var" : "The variable to check"], amode : is_sbdd_var(?), desc : html(" Succeeds iff Var is an SBDD variable (i.e. has been initialised through\n a call to sbdd_initialise/5).\n")]). :- comment(sbdd_indomain / 1, [summary : "Instantiate an integer SBDD variable to an element of its domain", args : ["Var" : "The (integer) SBDD variable to instantiate, or an integer"], amode : sbdd_indomain(?), see_also : [indomain / 1, sbdd_try / 2, sbdd_labeling / 1], desc : html(" Like indomain/1, but uses sbdd_try/2 to do the instantiation so that the\n SBDD dominance checks are performed appropriately.\n")]). :- comment(sbdd_initialise / 5, [summary : "Initialises the data structures required by the SBDD algorithm", args : ["Array" : "Array of (integer) decision variables", "VarDimNames" : "Names for the dimensions of Array", "ValueDimSpec" : "Name of the value dimension and its range", "SymSpecs" : "List of symmetry specifiers", "Options" : "List of extra options"], amode : sbdd_initialise(+, ++, ++, +, +), see_also : [sbdd_initialise_set / 5, construct_group / 8, struct(sbdd_shared), sbdd_try / 2, sbdd_try / 3], desc : html(" Sets up the data structures required to perform an SBDD search. Array is\n an array containing the (integer) search variables, SymSpecs defines the\n symmetries of the problem, with VarDimNames and ValueDimSpec providing\n some extra required information; these four arguments are the same as the\n first four arguments of construct_group/8: please see the documentation\n for that predicate for a complete description of these arguments and\n details of the supported symmetry specifiers.
\n\n Options is a list of options which modify the way the search progresses.\n Currently only one option is supported: throttle(ThrottlePred). This\n option can be used to control whether or not the SBDD dominance check is\n invoked at any given node. At each node, before performing the dominance\n check, ThrottlePred is called with an extra argument appended, and if the\n call fails, the dominance check is skipped. The extra argument is the\n sbdd_shared data structure, which holds the current state of the SBDD\n search; its fields can be examined (e.g. the current search depth) in\n order to decide whether to proceed with the dominance check or not.
\n\n During search, use sbdd_try/2 or sbdd_try/3 on variables from Array when\n making search decisions.\n")]). :- comment(sbdd_initialise_set / 5, [summary : "Initialises the data structures required by the SBDD algorithm (set version)", args : ["Array" : "Array of integer set decision variables", "VarDimNames" : "Names for the dimensions of Array", "ValueDimSpec" : "Name of the value dimension and its range", "SymSpecs" : "List of symmetry specifiers", "Options" : "List of extra options"], amode : sbdd_initialise_set(+, ++, ++, +, +), see_also : [sbdd_initialise / 5, sbdd_try_set / 3, sbdd_try_set / 4], desc : html(" Like sbdd_initialise/5, but for set models (i.e. Array should be an array\n of integer set variables). The \"value\" dimension is the values that can \n appear in the set, so that, for example, a range of 1..5 indicates that\n the upper bound of the set variables is [1,2,3,4,5].
\n\n See the documentation for sbdd_initialise/5 for more details.\n\n During search, use sbdd_try_set/3 or sbdd_try_set/4 on variables from\n Array when making search decisions.\n")]). :- comment(sbdd_labeling / 1, [summary : "Instantiate all integer SBDD variables in a list to elements of their domains", args : ["List" : "A list of integer SBDD variables or integers"], amode : sbdd_labeling(?), see_also : [labeling / 1, sbdd_indomain / 1], desc : html(" Like labeling/1, but uses sbdd_indomain/1 to do the instantiation so that\n the SBDD dominance checks are performed appropriately.\n")]). :- comment(sbdd_try / 2, [summary : "Try assigning a value to an SBDD search variable", args : ["Var" : "The variable to use", "Value" : "The value to try"], amode : sbdd_try(+, ++), see_also : [sbdd_initialise / 5, sbdd_try / 3], desc : html(" Make an SBDD search choice. Specifically, try assigning the (integer)\n value Value to the variable Var; on backtracking exclude the value Value\n from the domain of Var.
\n\n Var should be an element of an array previously initialised using\n sbdd_initialise/5.
\n\n Use sbdd_try/3 if you wish to know which is the currently successful\n branch (Var #= Value or Var #\\= Value).\n")]). :- comment(sbdd_try / 3, [summary : "Try assigning a value to an SBDD search variable", args : ["Var" : "The variable to use", "Value" : "The value to try", "Success" : "Whether the assignment succeeded or not"], amode : sbdd_try(+, ++, ?), see_also : [sbdd_initialise / 5, sbdd_try / 2], desc : html(" Like sbdd_try/2, but assign 1 to Success if we have set Var #= Value, and\n assign 0 if we have set Var #\\= Value (effectively, Success reflects the\n truth of Var #= Value when the predicate succeeds).
\n\n See the documentation for sbdd_try/2 for more details.\n")]). :- comment(sbdd_try_set / 3, [summary : "Try adding/excluding a value to/from an SBDD set search variable", args : ["Var" : "The set variable to use", "Value" : "The value to try", "Bool" : "Whether to add or exclude the value first"], amode : sbdd_try_set(+, ++, ++), see_also : [sbdd_initialise_set / 5, sbdd_try_set / 4, sbdd_try / 2], desc : html(" Make an SBDD (set) search choice. Specifically, if Bool is 1, try adding\n the (integer) value Value to the (set) variable Var; on backtracking\n exclude it. If Bool is 0, try excluding Value first and try adding it on\n backtracking.
\n\n Var should be an element of an array previously initialised using\n sbdd_initialise_set/5.
\n\n Use sbdd_try_set/4 if you wish to know which is the currently successful\n branch (Value in Var or Value notin Var).\n")]). :- comment(sbdd_try_set / 4, [summary : "Try adding/excluding a value to/from an SBDD set search variable", args : ["Var" : "The set variable to use", "Value" : "The value to try", "Bool" : "Whether to add or exclude the value first", "Success" : "Whether the assignment succeeded or not"], amode : sbdd_try_set(+, ++, ++, ?), see_also : [sbdd_initialise_set / 5, sbdd_try_set / 3, sbdd_try / 3], desc : html(" Like sbdd_try_set/3, but assign 1 to Success if we have Value in Var, and\n assign 0 if we have Value notin Var (effectively, Success reflects the\n truth of Value in Var when the predicate succeeds).
\n\n See the documentation for sbdd_try_set/3 for more details.\n")]). :- comment(throttle_default / 1, [summary : "Default throttling predicate", args : ["SBDDInfo" : "The sbdd_shared data structure"], amode : throttle_default(+), see_also : [sbdd_initialise / 5, sbdd_initialise_set / 5, throttle_depth_unique / 2, throttle_depth_non_unique / 2, throttle_depth_mod_unique / 2, throttle_depth_mod_non_unique / 2], desc : html(" Default throttling predicate used if none is given to sbdd_initialise/5\n or sbdd_initialise_set/5. This predicate simply succeeds, meaning that\n a dominance check is performed at every node in the search tree.\n")]). :- comment(throttle_depth_mod_non_unique / 2, [summary : "Example throttling predicate", args : ["DepthModulus" : "Depth modulus", "SBDDInfo" : "The sbdd_shared data structure"], amode : throttle_depth_mod_non_unique(++, +), see_also : [sbdd_initialise / 5, sbdd_initialise_set / 5, throttle_default / 1, throttle_depth_unique / 2, throttle_depth_non_unique / 2, throttle_depth_mod_unique / 2], desc : html(" Throttling predicate for use as an option to sbdd_initialise/5\n or sbdd_initialise_set/5. This predicate succeeds if the search depth is\n a multiple of DepthModulus. Note that this means that solutions found\n are not guaranteed to be unique.\n")]). :- comment(throttle_depth_mod_unique / 2, [summary : "Example throttling predicate", args : ["DepthModulus" : "Depth modulus", "SBDDInfo" : "The sbdd_shared data structure"], amode : throttle_depth_mod_unique(++, +), see_also : [sbdd_initialise / 5, sbdd_initialise_set / 5, throttle_default / 1, throttle_depth_unique / 2, throttle_depth_non_unique / 2, throttle_depth_mod_non_unique / 2], desc : html(" Throttling predicate for use as an option to sbdd_initialise/5\n or sbdd_initialise_set/5. This predicate succeeds if the search depth is\n a multiple of DepthModulus, or if the variable array is ground (ensuring\n solutions are guaranteed to be unique).\n")]). :- comment(throttle_depth_non_unique / 2, [summary : "Example throttling predicate", args : ["MaxDepth" : "Cut-off depth", "SBDDInfo" : "The sbdd_shared data structure"], amode : throttle_depth_non_unique(++, +), see_also : [sbdd_initialise / 5, sbdd_initialise_set / 5, throttle_default / 1, throttle_depth_unique / 2, throttle_depth_mod_unique / 2, throttle_depth_mod_non_unique / 2], desc : html(" Throttling predicate for use as an option to sbdd_initialise/5\n or sbdd_initialise_set/5. This predicate succeeds if the search depth\n does not exceed MaxDepth. Note that this means that solutions found are\n not guaranteed to be unique.\n")]). :- comment(throttle_depth_unique / 2, [summary : "Example throttling predicate", args : ["MaxDepth" : "Cut-off depth", "SBDDInfo" : "The sbdd_shared data structure"], amode : throttle_depth_unique(++, +), see_also : [sbdd_initialise / 5, sbdd_initialise_set / 5, throttle_default / 1, throttle_depth_non_unique / 2, throttle_depth_mod_unique / 2, throttle_depth_mod_non_unique / 2], desc : html(" Throttling predicate for use as an option to sbdd_initialise/5\n or sbdd_initialise_set/5. This predicate succeeds if the search depth\n does not exceed MaxDepth, or if the variable array is ground (ensuring\n solutions are guaranteed to be unique).\n")]). :- comment(first_solution_body / 2, hidden). :- comment(all_solutions_body / 3, hidden). :- comment(all_solutions_body / 2, hidden). :- comment(sbdd_initialise_set_body / 6, hidden). :- comment(sbdd_initialise_body / 6, hidden).